(* Spi-calculus data-structure *)
type name = string;;
type label = string;;
type msg = Name of string
	   | Encr of msg*msg
	   | MPair of msg*msg
	   | Ok;;
type reso = Reso of label*msg
            | RPair of reso*reso
            | Empty;;
type typ = Un
	   | Key of typ
	   | Ch of typ
	   | TPair of name*typ*typ
	   | TOk of reso
           | Unknown;;
type proc = Out of msg*msg
	    | In of msg*name*proc
	    | InRepl of msg*name*proc
	    | Nu of name*typ*proc
	    | PPara of proc*proc
	    | PNil
	    | Begin of label*msg
	    | End of label*msg
	    | Decrypt of msg*name*typ*msg*proc
	    | Split of msg*name*typ*name*typ*proc
	    | Match of msg*typ*msg*name*typ*proc;;

(* Each element in an environment is either a type or an effect *)
type env_element = Type of name*typ
	   | Effect of reso;;

(* "Pretty-printing" functions for error-messages and similar.
 * Note that these functions should, theoretically, print in a
 * syntax accepted by the parser.
 *)
let rec string_of_msg msg =
  match msg with
    | Name(x) -> x
    | Encr(m, n) -> Printf.sprintf "{%s}%s" (string_of_msg m) (string_of_msg n)
    | MPair(m, n) -> Printf.sprintf "pair(%s, %s)" (string_of_msg m) (string_of_msg n)
    | Ok -> "ok";;

let rec string_of_reso reso =
  match reso with
    | Reso(l, m) -> Printf.sprintf "%s(%s)" l (string_of_msg m)
    | RPair(r, s) -> Printf.sprintf "(%s, %s)" (string_of_reso r) (string_of_reso s)
    | Empty -> "Empty";;

let rec string_of_typ typ =
  match typ with
    | Un -> "Un"
    | Key(t) -> Printf.sprintf "Key(%s)" (string_of_typ t)
    | Ch(t) -> Printf.sprintf "Ch(%s)" (string_of_typ t)
    | TPair(x, t, u) -> Printf.sprintf "Pair(%s:%s, %s)" x (string_of_typ t) (string_of_typ u)
    | TOk(r) -> Printf.sprintf "Ok(%s)" (string_of_reso r)
    | Unknown -> "*";;

let rec string_of_proc proc =
  match proc with
    | Out(m, n) -> Printf.sprintf "out(%s, %s)" (string_of_msg m) (string_of_msg n)
    | In(m, x, p) -> Printf.sprintf "in(%s, %s); %s" (string_of_msg m) x (string_of_proc p)
    | InRepl(m, x, p) -> Printf.sprintf "!in(%s, %s); %s" (string_of_msg m) x (string_of_proc p)
    | Nu(x, t, p) -> Printf.sprintf "new %s:%s; %s" x (string_of_typ t) (string_of_proc p)
    | PPara(p, q) -> Printf.sprintf "(%s| %s)" (string_of_proc p) (string_of_proc q)
    | PNil -> "nil"
    | Begin(l, m) -> Printf.sprintf "begin %s(%s)" l (string_of_msg m)
    | End(l, m) -> Printf.sprintf "end %s(%s)" l (string_of_msg m)
    | Decrypt(m, x, t, n, p) -> Printf.sprintf "decrypt %s as {%s:%s}%s; %s" (string_of_msg m) x (string_of_typ t) (string_of_msg n) (string_of_proc p)
    | Split(m, x, t, y, u, p) -> Printf.sprintf "split %s as (%s:%s, %s:%s); %s" (string_of_msg m) x (string_of_typ t) y (string_of_typ u) (string_of_proc p)
    | Match(m, t, n, x, usub, p) -> Printf.sprintf "match %s:%s as (%s, %s:%s); %s" (string_of_msg m) (string_of_typ t) (string_of_msg n) x (string_of_typ usub) (string_of_proc p);;

let rec string_of_env_element env_element =
  match env_element with
    | Type(x, t) -> Printf.sprintf "%s:%s" x (string_of_typ t)
    | Effect(r) -> (string_of_reso r);;

let rec string_of_env env =
  List.fold_right (fun element env_str ->
		     (string_of_env_element element) ^ ", " ^ env_str) env "";;
